Nuprl Definition : ring_divs
13,42
postcript
pdf
a
|
b
in
r
==
c
:|
r
|. ((
c
*
a
) =
b
)
latex
clarification:
a
|
b
in
r
==
c
:|
r
|. ((
c
(*
r
)
a
) =
b
|
r
|)
latex
Up
rings
1
Wellformedness Lemmas
ring
divs
wf
Definitions
x
:
A
.
B
(
x
)
,
|
r
|
,
x
f
y
,
*
origin
c:|r|. ((c * a) = b)
c:|r|. ((c (*r) a) = b 
|r|) c:|r|. ((c * a) = b)
c:|r|. ((c (*r) a) = b |r|) x:A. B(x)